package org.eclipse.iota.junit;

import static org.eclipse.iota.bounds.BoundType.LOWER;
import static org.eclipse.iota.bounds.BoundType.UPPER;
import static org.junit.Assert.assertTrue;

import org.eclipse.iota.IotaPackage;
import org.eclipse.iota.evaluator.IotaEvaluator.EvaluationException;
import org.eclipse.iota.assignments.Assignment;
import org.eclipse.iota.bounds.Bound;
import org.eclipse.iota.bounds.BoundType;
import org.eclipse.iota.bounds.IotaBoundUtil;
import org.eclipse.iota.bounds.IotaRangeCalculator;
import org.eclipse.iota.bounds.OldIotaBoundCalculator;
import org.eclipse.iota.bounds.Range;
import org.eclipse.iota.model.Clause;
import org.eclipse.iota.model.Constant;
import org.eclipse.iota.model.Equation;
import org.eclipse.iota.model.EquationType;
import org.eclipse.iota.model.Expression;
import org.eclipse.iota.model.Parameter;
import org.eclipse.iota.model.Property;
import org.eclipse.iota.model.Reference;
import org.eclipse.iota.model.Variable;
import org.junit.Test;

/**
 * @author Christian Krause
 * @generated NOT
 */
@SuppressWarnings("deprecation")
public class BoundsCorrectnessTest extends AbstractIotaTest {
	
	@Test
	public void testBounds() {
		
		// Initialize the generator.
		generator.initWithDefaults();
		generator.getExpressionTypes().remove(IotaPackage.eINSTANCE.getDivision());
		
		// Create a range calculator:
		IotaRangeCalculator calculator = new IotaRangeCalculator();
		
		Constant[] lower = new Constant[EXPR_VARIABLES];
		Constant[] upper = new Constant[EXPR_VARIABLES];
		Equation[] equations = new Equation[EXPR_VARIABLES];
		
		for (int j=0; j<TESTS; j++) {
			
			Property property = generatePredicate(EXPR_VARIABLES, EXPR_DEPTH, EXPR_OPERANDS);
			Clause clause = property.getBody().getClauses().get(0);
			calculator.setClause(clause);
			calculator.clear();
			
			System.out.println("\nCalculating ranges for " + clause + "...");
			System.out.print("Ranges:");
			
			for (int i=0; i<property.getParameters().size(); i++) {
				
				Parameter variable = property.getParameters().get(i);
				Reference ref = new Reference(variable);
				
				// Old style:
				lower[i] = OldIotaBoundCalculator.calculateLowerBound(ref, clause);
				upper[i] = OldIotaBoundCalculator.calculateUpperBound(ref, clause);
				equations[i] = (Equation) clause.getConstraints().get(i);
				
				// New style:
				Range range = calculator.map(ref);
				System.out.print(" " + ref + ": " + range);
				
				if (lower[i]!=null) {
					Bound l = range.getLowerBound();
					assertTrue("New calculator failed at lower bound: " + l + " should be " + lower[i], l!=null);
				}
				if (upper[i]!=null) {
					Bound u = range.getUpperBound();
					assertTrue("New calculator failed at upper bound: " + u + " should be " + upper[i], u!=null);
				}
				
				lower[i] = range.getLowerBound().getValue();
				upper[i] = range.getUpperBound().getValue();				
			}
			
			assertTrue("Bounds test for " + clause + " failed.", testBounds(EVALUATIONS, equations, lower, upper));
			
		}
		
	}
	
	
	protected Property generatePredicate(int vars, int depth, int operands) {
		
		// Initialize predicate and clause.
		Property property = new Property("boundsTest");		
		Clause clause = new Clause();
		property.getBody().getClauses().add(clause);
		
		for (int i=0; i<vars; i++) {
			
			// Generate an expression.
			Expression expression = generator.generateExpression(depth, operands, clause);
			
			// Add a new parameter to the predicate.
			Parameter param = new Parameter(String.valueOf((char) ('a'+i)));
			property.getParameters().add(param);
			
			// Add an equation to the clause.
			int type = (int) (Math.random() * 3);
			Equation equation = new Equation(new Reference(param), expression, EquationType.get(type));
			clause.getConstraints().add(equation);
			
		}
		
		return property;
		
	}
	
	
	protected boolean testBounds(int tests, Equation[] equations, Constant[] lower, Constant[] upper) {
		
		int passed = 0;
		
		for (int i=1; i<equations.length; i++) {
			
			// Nothing to test?
			if (lower[i]==null && upper[i]==null) continue;
			
			Variable variable = ((Reference) equations[i].getLeft()).getVariable();
			Expression expression = equations[i].getRight();
			
			for (int test=0; test<tests; test++) {
				
				// Create a valid assignment;
				Assignment assignment = new Assignment();				
				for (int j=0; j<i; j++) {
					Constant value = Constant.random(lower[j], upper[j]);
					Variable current = ((Reference) equations[j].getLeft()).getVariable();
					assignment.put(current, value);
				}
				
				// Evaluate the current expression.
				evaluator.setAssignment(assignment);
				//System.out.println("Testing assignment " +assignment + "...");
				
				try {
					
					Equation lowerTest = makeBoundTest(equations[i].getRight(), LOWER); 
					Equation upperTest = makeBoundTest(equations[i].getRight(), UPPER); 
					
					boolean lowerok = (lowerTest==null || evaluator.evaluate(lowerTest).getValue());
					boolean upperok = (upperTest==null || evaluator.evaluate(upperTest).getValue());
					
					if (!lowerok || !upperok) {
						System.out.println("--- ERROR FOUND: ");
						System.out.println("--- Variable:   " + variable);
						System.out.println("--- Expression: " + expression);
						System.out.println("--- Assignment: " + assignment);
						System.out.println("--- Lower test: " + lowerTest);
						System.out.println("--- Upper test: " + upperTest);						
						System.out.println("--- Lower ok:   " + lowerok);
						System.out.println("--- Upper ok:   " + upperok);
						return false;
					}
					
					if (lowerTest!=null) passed++;
					if (upperTest!=null) passed++;
					
				} catch (EvaluationException e) {
					System.err.println(e);
					//e.printStackTrace();
				}
				
			}
		}
		
		return true;
		
	}
	
	private Equation makeBoundTest(Expression expression, BoundType type) {
		Constant bound = OldIotaBoundCalculator.calculateBound(expression, expression.getEquation().getClause(), type);
		if (bound!=null) return IotaBoundUtil.makeConstraint(expression, bound, type);
		else return null;
	}

}
